@$i$: only $L$ affects $x$ : $t$($j$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$) then only members of $L$ affect $x$ :$t$ else fi